$\forall$${\it es}$:ES, $A$:Type, ${\it Ia}$:AbsInterface($A$). $\lambda$$e$.$e$'${\it Ia}$ = ${\it Ia}$